
-- Module Definition
module Flminimodelcheckerv1 where

import Array
--import Control.Monad.ST
--import Data.STRef
--import Control.Monad

-- Type definition
type Vertex = Char
type Table a = Array Vertex a
type Graph = Table [Vertex]

-- Function definition
vertices :: Graph -> [Vertex]
vertices = indices

-- Type definition
type Edge = (Vertex, Vertex)

-- Function definition
edges :: Graph -> [Edge]
edges g = [(v, w) | v <- vertices g, w <- g ! v] 

mapT :: (Vertex -> a -> b) -> Table a -> Table b
mapT f t = array (bounds t)
				[(v, f v (t!v)) | v <- indices t]

-- Type definition
type Bounds = (Vertex, Vertex)

-- Function definition
outdegree :: Graph -> Table Int
outdegree g = mapT numEdges g
	where numEdges v ws = length ws



-- Function Definition
-- Build up a graph from a list of edges
buildG :: Bounds -> [Edge] -> Graph
buildG bnds es = accumArray (flip (:)) [] bnds es

-- Function Definition
-- Reverse all the edges in a graph
transposeG :: Graph -> Graph
transposeG g = buildG (bounds g) (reverseE g)

-- Function Definition
-- Reverse all the edges in a graph
reverseE :: Graph -> [Edge]
reverseE g = [(w, v) | (v, w) <- edges g]

-- Function definition
indegree :: Graph -> Table Int
indegree g = outdegree (transposeG g)

-- Type definition
data Tree a = Node a (Forest a)
type Forest a = [Tree a]


-- Function definition
-- Require: a graph g and a vertex v
-- Return:  a tree rooted at v containing all the vertices in g reachable from v
generate :: Graph -> Vertex -> Tree Vertex
generate g v = Node v (map (generate g) (g!v))

-- Type definition
data Set s = MutArr s Vertex Bool

-- Type definition
type ST s a = s -> (a, s)

-- Function definition
returnST :: a -> ST s a
returnST a s = (a, s)

thenST :: ST s a -> (a -> ST s b) -> ST s b
m `thenST` k = k a t  where  (a, t) = m s

newArr :: Ix i => (i,i) -> a -> ST s (MutArr s i a)
readArr :: Ix i => MutArr s i a -> i -> ST s a
writeArr :: Ix i => MutArr s i a -> a -> ST s () 




-- Function Definition
mkEmpty :: Bounds -> ST s (Set s)
mkEmpty bnds = newArr bnds False

contains :: Set s -> Vertex -> ST s Bool
contains m v = readArr m v

include :: Set s -> Vertex -> ST s ()
include m v = writeArr m v True

prune :: Bounds -> Forest Vertex -> Forest Vertex
prune bnds ts =
	runST (mkEmpty bnds `thenST` \m -> chop m ts)
	
chop :: Set s -> Forest Vertex -> ST s (Forest Vertex)
chop m [] = restureST []
chop m (Node v ts : us)
	= contains m v `thenST` \visited ->
		if visited then
			chop m us
		else 
			include m v	`thenST` \_ ->
			chop m ts	`thenST` \as ->
			chop m us   `thenST` \bs ->
			returnST ((Node v as) : bs)

-- Function definition
-- Depth-First Search
-- dfs :: Graph -> [Vertex] -> Forest Vertex
dfs g vs = prune (bounds g) (map (generate g) vs)


-- Exampe of graph

graph = buildG ('a', 'j') [('a','j'),('a', 'g'),('b','i'),('b','a'),('c','h'),('c','e'),('e','j'),('e','h'),('e','d'),('f','i'),('g','f'),('g','b')]